(declare-fun str2 () String)
(declare-fun str3 () String)
(declare-fun str6 () String)
(declare-fun str7 () String)
(declare-fun str8 () String)
(declare-fun str10 () String)
(declare-fun str11 () String)
(declare-fun str12 () String)
(declare-fun v19 () Bool)
(assert (= v19 (and (= str2 str10) (= str2 str7))))
(assert (distinct str11 str3 "u0" str8))
(assert (= (= v19 (and v19 (= str2 str10))) (and (= str11 (str.++ str8 str6)) (= (str.++ str8 str6) (str.++ str12 str3 str2)))))
(push)
(check-sat)
(pop)
(check-sat)
